r:Rng, a, b, c:|r|. (a +r (b +r c)) = (b +r (a +r c))  |r| 

latex

Up	rings 1
Definitions of Statement	Rng, r+gp
Definitions	IMonoid, t  T, IAbMonoid, x f y, x:A. B(x), t.2, t.1, , P & Q, Mon, Group{i}, AbGrp, r+gp, *, |g|
Lemmas	rng wf, abgrp wf, comm wf, grp id wf, grp op wf, grp car wf, monoid p wf, add grp of rng wf b, abmonoid ac 1